The vdm style option aids typesetting of VDM specifications: it provides macros for typesetting formulae, data types, functions, operations and proofs in whatever the currently approved VDM manner happens to be. A copy of the user manual for the vdm style option can be obtained by typing
latex /usr/lib/tex/macros/vdm.tex